T, A:Type, P:(AT), k:Knd, i, r, x:Id, es:ES. recognizer-p(es;T;A;P;k;i;r;x)   

latex

Definitions	P  Q, {T}, SQType(T), x. t(x), A c B, x:A. B(x), P  Q, @i(x:T), P  Q, P & Q, recognizer-p(es;T;A;P;k;i;r;x), , t  T, Knd, x:A. B(x), x(s), e@i. P(e)
Lemmas	bool wf, IdLnk wf, event system wf, es-val wf, es-le-loc, Id sq, es-after wf, iff wf, es-when wf, es-isconst wf, assert wf, es-vartype wf, es-loc wf, Id wf, es-E wf, es-valtype wf, subtype rel wf, es-kind wf, Knd wf, alle-at wf